Inference at * 
Iof proof for Lemma p-compose-id:


  A, B:Type, f:(A(B + Top)). f o p-id()   = f 

latex

 by (Auto) 
CollapseTHEN ((RepUR ``p-compose p-id can-apply do-apply`` ( 0)) 
CollapseTHEN ((
CExt) 
CollapseTHEN ((Reduce 0) 
CollapseTHEN (Auto)))) 

latex

C.

Definitions

Type, x:A. B(x), s = t, x:AB(x), left + right, Top, p-id(), f o g  , can-apply(f;x), do-apply(f;x), f(a), x.A(x)